COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	STANFORD ARTIFICIAL INTELLIGENCE LABORATORY
C00004 00003	FORMAL REASONING (Part 1)
C00007 00004	FORMAL REASONING (Part 2)
C00012 00005	LANGUAGE UNDERSTANDING
C00015 00006	PROGRAM VERIFICATION:
C00021 00007	AUTOMATED MATHEMATICS
C00023 ENDMK
C⊗;
STANFORD ARTIFICIAL INTELLIGENCE LABORATORY

	Here is our report on recent work.  I can summarize it as follows:
1. McCarthy has made what he thinks is a major theoretical breakthrough
in the representation of knowledge about knowledge.  Otherwise the
work in formal reasoning is proceeding about as planned.  In particular,
the proof of correctness of the McCarthy-Painter compiler is not much
longer than informal proof in the paper.

2. Winograd and his students and collaborators at Xerox have preliminary
versions of their KRL knowledge representation language.  This
is the main attempt to extend the ideas of Winograd's famous thesis
to a general capability.

3. Luckham continues to extend his program verification methods
to ever more realistic problems including those of verifying operating
systems.

4. Lenat (these results are more fully reported by Feigenbaum) has
had considerable success in generating mathematical results and
checking them for "interest".  This may also be a major breakthrough,
but the limits of his techniques have to be checked.

The following pages contain brief writeups by the group leaders and researchers:

FORMAL REASONING (Part 1)

	We think we have made a major breakthrough in the representation
of knowledge about knowledge and related topics.  Its importance
comes from the fact that intelligent systems must reason about what
they know and what other people and machines know and where information
is to be found.  To give a military example, a program intended to
help predict enemy action must reason about what the enemy knows,
believes and wants.  It must also reason about what it wants to know
and whether it can hope to find out by reasoning or must seek external
sources of information.  The ability to reason about
sources of information is important in all areas of artificial intelligence.

	The advance consists in introducing concepts as mathematical
objects and introducing functions that have concepts as values along
with the functions that have things as values.  This permits treating
knowledge, belief, intention, wanting, etc. in ordinary first order
logic for which a good theory and powerful programs already exist
rather than in modal logic which is much less satisfactory and
for which programs don't exist.  The new way of handling knowledge
can also be used by PLANNER-like systems and probably by production
systems as well.

	The main ideas were developed by McCarthy in May and are
being actively pursued by him and his students Robert Moore and
Christopher Goad.

	A preliminary version of a Stanford AI Memo is
contained in the file CONCEP[S76,JMC], but the section on applications
to artificial intelligence is not yet incorporated.
FORMAL REASONING (Part 2)

The formal reasoning group at Stanford is primarily interested in
how general reasoning can be done using computers.  This requires 
both an understanding of how to make proper deductions and how to
represent the information content of common knowledge.  Our major
software effort has been a computer program, FOL, which serves as
an environment for experimenting with computer reasoning.  

During the past six months we have used FOL to prove the correctness 
of the McCarthy-Painter compiling algorithm, and to check the proofs
of about 100 theorems of mathematics.  These particular tasks were
chosen in order to give us information about what the formal proofs
of informally well understood theorems look like.  These proofs, as
well as some of those done last year, are being carefully examined
to analyze how well this particular computer representation of 
reasoning behaves and in what ways it can be improved.  The ultimate
aim is to find a general theory of computer reasoning.  As a result of 
similiar studies done late last year on the relation between solving 
problems by reasoning and observing things in the real world, 
we designed a new semantic attachment mechanism for FOL, which 
allows us a greater flexibility to do either.  This is presently 
being implemented, but is not yet running.  Several other improvements 
either have been or are being coded.

One reason for looking at proofs in mathematics and about programing 
languages is that the informal methods of reasoning about them 
have already been formalized, so we have a starting place for computer
reasoning.  Unfortunately, there are many areas of ordinary discourse
for which this formalization has not been as well carried out.  For
example, it is difficult to reason about other people's belief systems,
or to make deductions about what I know you know.  There are presently 
three people working on new axiomatizations of this kind of reasoning.
Substantial recent progress has been made on axiomatizing knowledge.

Accomplishments in the last six months.

1.  New version of FOL.  (April)
2.  McCarthy Painter compiler proved correct using FOL.	
3.  100 propositions of Kelly set theory proved using FOL.
4.  Design of new semantic attachment mechanism. (coding almost complete)
5.  Design of subgoaling facility. (some code runs but none on system)
6.  Design of SWITCH routines. (code runs, but not on system)
7.  Implementation of Sussman and Steele like SCHEME.
   	a. for call by value interpreter.
	b. for call by name interpreter.
8.  Axiomatization of the metamathematics of binary trees.
9.  Axiomatization of reasoning about knowledge.

LANGUAGE UNDERSTANDING

The research of the language understander group, directed by
Terry Winograd and supported by several sources, is guided
by the belief that more powerful and flexible representational
tools are needed to construct programs which reason and use
natural language.  Over the last year, in conjunction with 
several other researchers,  we 
have been developing a Knowledge Representation Language.
This language is intended to facilitate the integration of
procedural and declarative knowledge, the representation and use
of partial knowledge, and the ability to reason by analogy.
In the initial implementation of this language, we have thus far
written and debugged two extensive test programs.  The first of
these is a language understanding system which accepts several
simple stories in English, then summarizes and answers questions
about them.  It demonstrates the capability in the language for 
representing large, related segments of real-world knowledge, 
and for integrating syntactic and semantic knowledge.  The
second program, a medical diagnosis system which accepts a
set of patient symtoms and responds with a set of explanatory
diseases, exercises the facilities provided in the language for
factoring knowledge along many dimensions, and reasoning from
partial information.
-------

PROGRAM VERIFICATION:

1.Methods for verifying programs containing operations on POINTERS
have been developed and implemented in the verifier. The verifier has been 
used to check the correctness of about 20 pointer programs including
a garbage collector and part of a scheduler (one page of Pascal code).

2. A study of the application of verifiers to the software maintainence
problem has been completed. A sophisticated sorting program, QUICKSORT,
which has many variants, was used. It was shown that the verifier
could prove the correctness of 6 variants of QUICKSORT using a single
standard set of specifications. Bugs were introduced into the code.
it was found that the user could quickly (7 minutes for 3 bugs)
identify the bugs from the output of the verifier without first
checking the code.

3.The verifier has been used to analyze the implementation of a basic
queuing system in an operating system [1]. A total of 31 specifications
of the queuing system were proved by the verifier (these required the
new proof rules for RECORDS and POINTERS). These results showed
(a) the queues would be maintained correctly under all circumstances,
(b) the queuing system was fair, but (c) there were situations in which
the queuing system would leave resources idle [2].
The verifier is currently being extended to handle PROTECTION and 
DEADLOCK problems in the SOLO operating system [3], a working
and widely distributed PDP-11 system.

4. New fast theorem provers using graph representations of data for
arithmetical problems and for pointer manipulation problems have been designed
and coded. These theorem provers are crucial subsystems of program verifiers.
Their response time directly reflects on the feasibilty of using
verifiers as programming aids.

[1] A. SAXENA and T. BREDT, "A structured specification of an operating
system", Proc. International Conference on Reliable Software, April 1975,
pp. 310-318.

[2] R. KARP and D. LUCKHAM, "Proof of Fairness in an implementaion of
Monitors", forthcoming International Conference on Software Engineering, Oct. 1976.

[3] P. BRINCH HANSEN, "The purpose of Concurrent Pascal"
Proc. International Conference on Reliable Software, April 1975,
pp. 305-309.



AUTOMATED MATHEMATICS

An  Artificial  Intelligence   computer  program  which   learns  new
elementary  mathematics by itself  has recently been  completed by D.
Lenat. This system, called "AM", has rediscovered several  basic math
concepts (e.g., prime numbers), and was instrumental in the discovery
of  one new result in elementary  number theory. AM views mathematics
as a collection of interrelated concepts. AM decides which concept to
define next,  determines the resources  to expend on  developing that
concept, and then judges the interestingness  of the new concept.   A
large knowledge base of elementary  mathematics knowledge is present,
in the form of  heuristic rules which are used to guide each of these
processes.   This project  represents a  significant  advance in  the
state of  the art  in symbolic learning  programs. It  is anticipated
that the technology developed will be applicable to computer learning
of new concepts in other, less theoretical domains.